$\forall$$w$:World, $e$:E.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ ($\uparrow$rcv?($e$))
\\[0ex]$\Rightarrow$ (msg(lnk(kind($e$));tag(kind($e$));val($e$)) $\in$ m(loc(sender($e$));time(sender($e$))))